$\forall$$l$:IdLnk, ${\it dt}$:fpf(Id; ${\it tg}$.Type), ${\it tg}$:Id. \\[0ex]sqequal(fpf{-}dom(Kind{-}deq; rcv($l$,${\it tg}$); lnk{-}decl($l$; ${\it dt}$)); fpf{-}dom(id{-}deq; ${\it tg}$; ${\it dt}$))